1 /-
2 Copyright (c) 2019 Jan-David Salchow. All rights reserved.
3 Released under Apache 2.0 license as described in the file LICENSE.
4 Authors: Jan-David Salchow, Sébastien Gouëzel, Jean Lo
5
6 Operator norm on the space of continuous linear maps
7
8 Define the operator norm on the space of continuous linear maps between normed spaces, and prove
9 its basic properties. In particular, show that this space is itself a normed space.
10 -/
11
12 import topology.metric_space.lipschitz analysis.normed_space.riesz_lemma
src └─────────────────────────────┘ └───────────────────────────────┘
13 import analysis.asymptotics
src └──────────────────┘
14 noncomputable theory
15 open_locale classical
16
17 set_option class.instance_max_depth 70
doc └──────────────────────┘
18
19 variables {𝕜 : Type*} {E : Type*} {F : Type*} {G : Type*}
20 [normed_group E] [normed_group F] [normed_group G]
21
22 open metric continuous_linear_map
23
24 lemma exists_pos_bound_of_bound {f : E → F} (M : ℝ) (h : ∀x, ∥f x∥ ≤ M * ∥x∥) :
25 ∃ N, 0 < N ∧ ∀x, ∥f x∥ ≤ N * ∥x∥ :=
26 ⟨max M 1, lt_of_lt_of_le zero_lt_one (le_max_right _ _), λx, calc
id └──────────┘ └─────────┘ └──────────┘ ┴
src └──────────┘ └─────────┘ └──────────┘
typ └──────────┘ └┘└───────┘ └──────────┘ ┴
27 ∥f x∥ ≤ M * ∥x∥ : h x
id ┴┴ ┴┴ ┴ ┴ ┴┴┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴┴ ┴┴ ┴ ┴ ┴┴┴ ┴ ┴
28 ... ≤ max M 1 * ∥x∥ : mul_le_mul_of_nonneg_right (le_max_left _ _) (norm_nonneg _) ⟩
id └─┘ ┴ ┴ ┴┴┴ └────────────────────────┘ └─────────┘ └─────────┘
src └─┘ ┴ ┴ ┴ └────────────────────────┘ └─────────┘ └─────────┘
typ └─┘ ┴ ┴ ┴┴┴ └────────────────────────┘ └─────────┘ └─────────┘
29
30 section normed_field
31 /- Most statements in this file require the field to be non-discrete, as this is necessary
32 to deduce an inequality `∥f x∥ ≤ C ∥x∥` from the continuity of f. However, the other direction always
33 holds. In this section, we just assume that `𝕜` is a normed field. In the remainder of the file,
34 it will be non-discrete. -/
35
36 variables [normed_field 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 F] (f : E →ₗ[𝕜] F)
id └──────────┘ └──────────┘ └──────────┘ └─┘ ┴
src └──────────┘ └──────────┘ └──────────┘ └─┘ ┴
typ └──────────┘ └──────────┘ └──────────┘ └─┘ ┴
doc └──────────┘ └──────────┘ └──────────┘
37
38 lemma linear_map.lipschitz_of_bound (C : ℝ) (h : ∀x, ∥f x∥ ≤ C * ∥x∥) :
id ┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴ ┴┴┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴ ┴┴┴
39 lipschitz_with (nnreal.of_real C) f :=
id └────────────┘ └────────────┘ ┴ ┴
src └────────────┘ └────────────┘
typ └────────────┘ └────────────┘ ┴ ┴
doc └────────────┘
40 lipschitz_with.of_dist_le $ λ x y, by simpa [dist_eq_norm] using h (x - y)
id └───────────────────────┘
src └───────────────────────┘ └─────┘ └──────┘ ┴ ┴ ┴ └─
typ └───────────────────────┘ └─────┘ └──────┘ ┴ ┴ ┴ └─
doc └─────┘ └──────┘ ┴ ┴ ┴ └─
txt └─────┘ └──────┘ ┴ ┴ ┴ └─
par └─────┘ └──────┘ ┴ ┴ ┴ └─
pid ┴┴ ┴┴└────┘ ┴ ┴ ┴ ┴└
41
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
42 lemma linear_map.uniform_continuous_of_bound (C : ℝ) (h : ∀x, ∥f x∥ ≤ C * ∥x∥) :
43 uniform_continuous f :=
44 (f.lipschitz_of_bound C h).to_uniform_continuous
45
46 lemma linear_map.continuous_of_bound (C : ℝ) (h : ∀x, ∥f x∥ ≤ C * ∥x∥) :
47 continuous f :=
48 (f.lipschitz_of_bound C h).to_continuous
49
50 /-- Construct a continuous linear map from a linear map and a bound on this linear map.
51 The fact that the norm of the continuous linear map is then controlled is given in
52 `linear_map.mk_continuous_norm_le`. -/
53 def linear_map.mk_continuous (C : ℝ) (h : ∀x, ∥f x∥ ≤ C * ∥x∥) : E →L[𝕜] F :=
54 ⟨f, linear_map.continuous_of_bound f C h⟩
55
56 /-- Construct a continuous linear map from a linear map and the existence of a bound on this linear
57 map. If you have an explicit bound, use `linear_map.mk_continuous` instead, as a norm estimate will
58 follow automatically in `linear_map.mk_continuous_norm_le`. -/
59 def linear_map.mk_continuous_of_exists_bound (h : ∃C, ∀x, ∥f x∥ ≤ C * ∥x∥) : E →L[𝕜] F :=
60 ⟨f, let ⟨C, hC⟩ := h in linear_map.continuous_of_bound f C hC⟩
61
62 @[simp, elim_cast] lemma linear_map.mk_continuous_coe (C : ℝ) (h : ∀x, ∥f x∥ ≤ C * ∥x∥) :
doc └──┘ └───────┘
63 ((f.mk_continuous C h) : E →ₗ[𝕜] F) = f := rfl
64
65 @[simp] lemma linear_map.mk_continuous_apply (C : ℝ) (h : ∀x, ∥f x∥ ≤ C * ∥x∥) (x : E) :
doc └──┘
66 f.mk_continuous C h x = f x := rfl
67
68 @[simp, elim_cast] lemma linear_map.mk_continuous_of_exists_bound_coe (h : ∃C, ∀x, ∥f x∥ ≤ C * ∥x∥) :
doc └──┘ └───────┘
69 ((f.mk_continuous_of_exists_bound h) : E →ₗ[𝕜] F) = f := rfl
70
71 @[simp] lemma linear_map.mk_continuous_of_exists_bound_apply (h : ∃C, ∀x, ∥f x∥ ≤ C * ∥x∥) (x : E) :
doc └──┘
72 f.mk_continuous_of_exists_bound h x = f x := rfl
73
74 lemma linear_map.continuous_iff_is_closed_ker {f : E →ₗ[𝕜] 𝕜} :
75 continuous f ↔ is_closed (f.ker : set E) :=
76 begin
77 -- the continuity of f obviously implies that its kernel is closed
78 refine ⟨λh, (continuous_iff_is_closed.1 h) {0} (t1_space.t1 0), λh, _⟩,
src └─────┘ └─┘ └─┘ └┘ └─┘ └───┘ └───┘
typ └─────┘ └─┘ └─┘ └┘ └─┘ └───┘ └───┘
doc └─────┘ └─┘ └─┘ └┘ └─┘ └───┘ └───┘
txt └─────┘ └─┘ └─┘ └┘ └─┘ └───┘ └───┘
par └─────┘ └─┘ └─┘ └┘ └─┘ └───┘ └───┘
pid ┴ └─┘ └─┘ └┘ └─┘ └───┘ └───┘
79 -- for the other direction, we assume that the kernel is closed
80 by_cases hf : ∀x, x ∈ f.ker,
src └───────┘ └─┘ ┴ ┴ ┴ ┴
typ └───────┘ └─┘ ┴ ┴ ┴ ┴
doc └───────┘ └─┘ ┴ ┴ ┴ ┴
txt └───────┘ └─┘ ┴ ┴ ┴ ┴
par └───────┘ └─┘ ┴ ┴ ┴ ┴
pid ┴ └─┘ ┴ ┴ ┴ ┴
81 { -- if `f = 0`, its continuity is obvious
82 have : (f : E → 𝕜) = (λx, 0), by { ext x, simpa using hf x },
src └─────┘ └─┘ ┴ ┴ └┘ ┴ └───┘ └───┘ └──────────┘ ┴ ┴
typ └─────┘ └─┘ ┴ ┴ └┘ ┴ └───┘ └───┘ └──────────┘ ┴ ┴
doc └─────┘ └─┘ ┴ ┴ └┘ ┴ └───┘ └───┘ └──────────┘ ┴ ┴
txt └─────┘ └─┘ ┴ ┴ └┘ ┴ └───┘ └───┘ └──────────┘ ┴ ┴
par └─────┘ └─┘ ┴ ┴ └┘ ┴ └───┘ └───┘ └──────────┘ ┴ ┴
pid └───┘└┘ └─┘ ┴ ┴ └┘ ┴ └───┘ └┘ ┴└────┘ ┴ ┴
83 rw this,
src └─┘
typ └─┘
doc └─┘
txt └─┘
par └─┘
pid ┴
84 exact continuous_const },
src └────┘ ┴
typ └────┘ ┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
85 { /- if `f` is not zero, we use an element `x₀ ∉ ker f` such that `∥x₀∥ ≤ 2 ∥x₀ - y∥` for all
86 `y ∈ ker f`, given by Riesz's lemma, and prove that `2 ∥f x₀∥ / ∥x₀∥` gives a bound on the
st └──────────────────────────────────────────────────────────────────────────────────────────
87 operator norm of `f`. For this, start from an arbitrary `x` and note that
st ──────────────────────────────────────────────────────────────────────────────
88 `y = x₀ - (f x₀ / f x) x` belongs to the kernel of `f`. Applying the above inequality to `x₀`
st ──────────────────────────────────────────────────────────────────────────────────────────────────
89 and `y` readily gives the conclusion. -/
st ─────────────────────────────────────────────
90 push_neg at hf,
src └────────────┘
typ └────────────┘
doc └────────────┘
txt └────────────┘
par └────────────┘
pid └────┘
st ─────────────────┘└─
91 let r : ℝ := (2 : ℝ)⁻¹,
id ┴ └┘
src └──────┘┴└──┘ └──┘ ┴└┘
typ └──────┘┴└──┘ └──┘ ┴└┘
doc └──────┘ └──┘ └──┘ ┴
txt └──────┘ └──┘ └──┘ ┴
par └──────┘ └──┘ └──┘ ┴
pid └───┘└─┘ └──┘ └──┘ ┴
st ─────────────────────────┘└─
92 have : 0 ≤ r, by norm_num [r],
id ┴ ┴ ┴
src └───────┘┴┴ └────────┘ ┴
typ └───────┘┴┴┴ └────────┘┴┴
doc └───────┘ ┴ └────────┘ ┴
txt └───────┘ ┴ └────────┘ ┴
par └───────┘ ┴ └────────┘ ┴
pid └───┘└──┘ ┴ └┘ ┴
st ───────────────┘ └─
93 have : r < 1, by norm_num [r],
id ┴ ┴ ┴
src └─────┘ ┴┴└┘ └────────┘ ┴
typ └─────┘┴┴┴└┘ └────────┘┴┴
doc └─────┘ ┴ └┘ └────────┘ ┴
txt └─────┘ ┴ └┘ └────────┘ ┴
par └─────┘ ┴ └┘ └────────┘ ┴
pid └───┘└┘ ┴ ┴┴ └┘ ┴
st ───────────────┘ └─
94 obtain ⟨x₀, x₀ker, h₀⟩ : ∃ (x₀ : E), x₀ ∉ f.ker ∧ ∀ y ∈ linear_map.ker f, r * ∥x₀∥ ≤ ∥x₀ - y∥,
id ┴ ┴ ┴ └───┘ └────────────┘ ┴ ┴ ┴ ┴ ┴ ┴
src └───────────────────────┘┴└─────┘ ┴┴┴ ┴ ┴└───┘┴ ┴ └───┘└────────────┘┴ ┴ ┴┴┴┴ ┴┴ ┴ ┴┴┴
typ └───────────────────────┘┴└─────┘┴┴┴┴ ┴ ┴└───┘┴ ┴ └───┘└────────────┘┴┴ ┴┴┴┴┴┴ ┴┴ ┴ ┴┴┴
doc └───────────────────────┘ └─────┘ ┴ ┴ ┴ ┴└───┘┴ ┴ └───┘└────────────┘┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
txt └───────────────────────┘ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
par └───────────────────────┘ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
pid └─────────────────┘ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
st ────────────────────────────────────────────────────────────────────────────────────────────────┘└─
95 from riesz_lemma h hf this,
id └─────────┘ ┴ └┘ └──┘
src └───┘└─────────┘┴ ┴ ┴
typ └───┘└─────────┘┴┴┴└┘┴└──┘
doc └───┘└─────────┘┴ ┴ ┴
txt └───┘ ┴ ┴ ┴
par └───┘ ┴ ┴ ┴
pid └───┘ ┴ ┴ ┴
st ───────────────────────────────┘└─
96 have : x₀ ≠ 0,
id └┘ ┴
src └─────┘ ┴┴└┘
typ └─────┘└┘┴┴└┘
doc └─────┘ ┴ └┘
txt └─────┘ ┴ └┘
par └─────┘ ┴ └┘
pid └───┘└┘ ┴ ┴┴
st ────────────────┘└─
97 { assume h,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid └──────┘
st ─────┘└──────┘└─
98 have : x₀ ∈ f.ker, by { rw h, exact (linear_map.ker f).zero },
id └┘ └───┘ ┴ └────────────┘ ┴
src └─────┘ ┴ ┴└───┘ └─┘ └────┘ └────────────┘┴ └─────┘
typ └─────┘└┘┴ ┴└───┘ └─┘┴ └────┘ └────────────┘┴┴└─────┘
doc └─────┘ ┴ ┴└───┘ └─┘ └────┘ └────────────┘┴ └─────┘
txt └─────┘ ┴ ┴ └─┘ └────┘ ┴ └─────┘
par └─────┘ ┴ ┴ └─┘ └────┘ ┴ └─────┘
pid └───┘└┘ ┴ ┴ ┴ ┴ ┴ └───┘└┘
st ──────────────────────┘ ┴└───┘└──────────────────────────────┘└┘└
99 exact x₀ker this },
id └───┘ └──┘
src └────┘ ┴ ┴
typ └────┘└───┘┴└──┘┴
doc └────┘ ┴ ┴
txt └────┘ ┴ ┴
par └────┘ ┴ ┴
pid ┴ ┴ ┴
st ──────────────────────┘└┘└
100 have rx₀_ne_zero : r * ∥x₀∥ ≠ 0, by { simp [norm_eq_zero, this], norm_num },
id ┴ └┘ └──────────┘ └──┘
src └─────────────────┘ ┴ ┴ ┴ └┘ └────┘└──────────┘└┘ ┴ └───────┘
typ └─────────────────┘┴┴ ┴ └┘ ┴ └┘ └────┘└──────────┘└┘└──┘┴ └───────┘
doc └─────────────────┘ ┴ ┴ ┴ └┘ └────┘ └┘ ┴ └───────┘
txt └─────────────────┘ ┴ ┴ ┴ └┘ └────┘ └┘ ┴ └───────┘
par └─────────────────┘ ┴ ┴ ┴ └┘ └────┘ └┘ ┴ └───────┘
pid └──────────────┘└─┘ ┴ ┴ ┴ ┴┴ ┴┴ └┘ ┴ ┴
st ──────────────────────────────────┘ ┴└────────────────────────┘└─────────┘└┘└
101 have : ∀x, ∥f x∥ ≤ (((r * ∥x₀∥)⁻¹) * ∥f x₀∥) * ∥x∥,
id ┴ ┴ └┘
src └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴
typ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ └┘ ┴ ┴┴└┘ └┘ ┴
doc └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴
txt └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴
par └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴
pid └───┘└┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴
st ─────────────────────────────────────────────────────┘└─
102 { assume x,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid └──────┘
st ─────┘└──────┘└─
103 by_cases hx : f x = 0,
id ┴ ┴
src └───────┘ └─┘ ┴ ┴ └┘
typ └───────┘ └─┘┴┴┴┴ └┘
doc └───────┘ └─┘ ┴ ┴ └┘
txt └───────┘ └─┘ ┴ ┴ └┘
par └───────┘ └─┘ ┴ ┴ └┘
pid ┴ └─┘ ┴ ┴ ┴┴
st ──────────────────────────┘└─
104 { rw [hx, norm_zero],
id └┘ └───────┘
src └──┘ └┘└───────┘┴
typ └──┘└┘└┘└───────┘┴
doc └──┘ └┘ ┴
txt └──┘ └┘ ┴
par └──┘ └┘ ┴
pid └┘ └┘ ┴
st ───────┘└────┘└─────────┘└──
105 apply_rules [mul_nonneg', norm_nonneg, inv_nonneg.2, norm_nonneg] },
id └─────────┘ └─────────┘ └────────┘ └─────────┘
src └───────────┘└─────────┘└┘└─────────┘└┘└────────┘└──┘└─────────┘└┘
typ └───────────┘└─────────┘└┘└─────────┘└┘└────────┘└──┘└─────────┘└┘
doc └───────────┘ └┘ └┘ └──┘ └┘
txt └───────────┘ └┘ └┘ └──┘ └┘
par └───────────┘ └┘ └┘ └──┘ └┘
pid └┘ └┘ └┘ └──┘ ┴┴
st ─────────────────────────────────────────────────────────────────────────┘└┘└
106 { let y := x₀ - (f x₀ * (f x)⁻¹ ) • x,
id └┘ ┴ ┴ ┴
src └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘┴┴
typ └───────┘ ┴ ┴ ┴└┘┴ ┴ ┴┴ ┴ └─┘┴┴┴
doc └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴
txt └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴
par └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴
pid └───┘┴└─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴
st ──────────────────────────────────────────┘└─
107 have fy_zero : f y = 0, by calc
id ┴ ┴ └──┘
src └─────────────┘ ┴ ┴ └┘ └──┘
typ └─────────────┘┴┴┴┴ └┘ └──┘
doc └─────────────┘ ┴ ┴ └┘ └──┘
txt └─────────────┘ ┴ ┴ └┘
par └─────────────┘ ┴ ┴ └┘
pid └──────────┘└─┘ ┴ ┴ ┴┴
st ─────────────────────────────┘ └──┘
108 f y = f x₀ - (f x₀ * (f x)⁻¹ ) * f x :
id ┴ └┘ ┴ ┴
typ ┴ └┘ ┴ ┴
109 by { dsimp [y], rw [f.map_add, f.map_neg, f.map_smul], refl }
id ┴
src └─────┘ ┴ └──┘ └┘ └┘ ┴ └───┘
typ └─────┘┴┴ └──┘└───────┘└┘└───────┘└┘└────────┘┴ └───┘
doc └─────┘ ┴ └──┘ └┘ └┘ ┴ └───┘
txt └─────┘ ┴ └──┘ └┘ └┘ ┴ └───┘
par └─────┘ ┴ └──┘ └┘ └┘ ┴ └───┘
pid ┴┴ ┴ └┘ └┘ └┘ ┴ ┴
st └──────────┘└─────────────┘└─────────┘└──────────┘└──────┘└┘
110 ... = 0 :
111 by { rw [mul_assoc, inv_mul_cancel hx, mul_one, sub_eq_zero_of_eq], refl },
id └───────┘ └────────────┘ └┘ └─────┘ └───────────────┘
src └──┘└───────┘└┘└────────────┘┴ └┘└─────┘└┘└───────────────┘┴ └───┘
typ └──┘└───────┘└┘└────────────┘┴└┘└┘└─────┘└┘└───────────────┘┴ └───┘
doc └──┘ └┘ ┴ └┘ └┘ ┴ └───┘
txt └──┘ └┘ ┴ └┘ └┘ ┴ └───┘
par └──┘ └┘ ┴ └┘ └┘ ┴ └───┘
pid └┘ └┘ ┴ └┘ └┘ ┴ ┴
st └──────────────┘└─────────────────┘└───────┘└─────────────────┘└──────┘└┘└
112 have A : r * ∥x₀∥ ≤ ∥f x₀∥ * ∥f x∥⁻¹ * ∥x∥, from calc
id ┴ └┘ ┴ ┴
src └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ └
typ └───────┘┴┴ ┴ ┴ ┴ ┴└┘ ┴ ┴ ┴┴ ┴ ┴ ┴ └───┘ └
doc └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ └
txt └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ └
par └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ └
pid └────┘└─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ └
st ─────────────────────────────────────────────────┘└───────────
113 r * ∥x₀∥ ≤ ∥x₀ - y∥ : h₀ _ (linear_map.mem_ker.2 fy_zero)
id ┴ └┘ ┴ └┘ └────────────────┘ └─────┘
src ─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └─┘ └────────────────┘└─┘ └─
typ ─────────┘┴┴ ┴ ┴ ┴ └┘┴ ┴┴ └─┘└┘└─┘ └────────────────┘└─┘└─────┘└─
doc ─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └─┘ └─┘ └─
txt ─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └─┘ └─┘ └─
par ─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └─┘ └─┘ └─
pid ─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └─┘ └─┘ └─
st ────────────────────────────────────────────────────────────────────
114 ... = ∥(f x₀ * (f x)⁻¹ ) • x∥ : by { dsimp [y], congr, abel }
id ┴
src ─────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ └─┘ └─┘└─────┘ ┴└┘└───┘└┘└───┘└─
typ ─────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ └─┘ └─┘└─────┘┴┴└┘└───┘└┘└───┘└─
doc ─────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ └─┘ └─┘└─────┘ ┴└┘ └┘└───┘└─
txt ─────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ └─┘ └─┘└─────┘ ┴└┘└───┘└┘└───┘└─
par ─────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ └─┘ └─┘└─────┘ ┴└┘└───┘└┘└───┘└─
pid ─────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ └─┘ └────────┘ └────────────────
st ───────────────────────────────────────────┘└──────────┘└─────┘└─────┘┴└
115 ... = ∥f x₀∥ * ∥f x∥⁻¹ * ∥x∥ :
id ┴ ┴
src ─────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──
typ ─────────────┘ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ └──
doc ─────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──
txt ─────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──
par ─────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──
pid ─────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──
st ─────────────────────────────────────────
116 by rw [norm_smul, normed_field.norm_mul, normed_field.norm_inv],
id └───────┘ └───────────────────┘ └───────────────────┘
src ───────────┘ ┴└──┘└───────┘└┘└───────────────────┘└┘└───────────────────┘┴
typ ───────────┘ ┴└──┘└───────┘└┘└───────────────────┘└┘└───────────────────┘┴
doc ───────────┘ ┴└──┘ └┘ └┘ ┴
txt ───────────┘ ┴└──┘ └┘ └┘ ┴
par ───────────┘ ┴└──┘ └┘ └┘ ┴
pid ───────────┘ └───┘ └┘ └┘ ┴
st ─────────────┘└────────────┘└─────────────────────┘└─────────────────────┘┴└─
117 calc
id └──┘
src └──┘
typ └──┘
doc └──┘
st ─────────────
118 ∥f x∥ = (r * ∥x₀∥)⁻¹ * (r * ∥x₀∥) * ∥f x∥ : by rwa [inv_mul_cancel, one_mul]
id ┴ └┘ ┴ ┴ └────────────┘ └─────┘
src └───┘└────────────┘└┘└─────┘└─
typ ┴ └┘ ┴ ┴ └───┘└────────────┘└┘└─────┘└─
doc └───┘ └┘ └─
txt └───┘ └┘ └─
par └───┘ └┘ └─
pid └┘ └┘ ┴└
st ───────────────────────────────────────────────────────┘└──────────────────┘└───────┘┴└
119 ... ≤ (r * ∥x₀∥)⁻¹ * (∥f x₀∥ * ∥f x∥⁻¹ * ∥x∥) * ∥f x∥ : begin
src ─────────┘
typ ─────────┘
doc ─────────┘
txt ─────────┘
par ─────────┘
pid ─────────┘
st ─────────┘└──────────────────────────────────────────────────────┘└─────
120 apply mul_le_mul_of_nonneg_right (mul_le_mul_of_nonneg_left A _) (norm_nonneg _),
id └────────────────────────┘ └───────────────────────┘ ┴ └─────────┘
src └────┘└────────────────────────┘┴ └───────────────────────┘┴ └──┘ └─────────┘└─┘
typ └────┘└────────────────────────┘┴ └───────────────────────┘┴┴└──┘ └─────────┘└─┘
doc └────┘ ┴ ┴ └──┘ └─┘
txt └────┘ ┴ ┴ └──┘ └─┘
par └────┘ ┴ ┴ └──┘ └─┘
pid ┴ ┴ ┴ └──┘ └─┘
st ───────────────────────────────────────────────────────────────────────────────────────────┘└─
121 exact inv_nonneg.2 (mul_nonneg' (by norm_num) (norm_nonneg _))
id └────────┘ └─────────┘ └─────────┘
src └────┘└────────┘└─┘ └─────────┘┴ ┴└──────┘└┘ └─────────┘└────
typ └────┘└────────┘└─┘ └─────────┘┴ ┴└──────┘└┘ └─────────┘└────
doc └────┘ └─┘ ┴ ┴└──────┘└┘ └────
txt └────┘ └─┘ ┴ ┴└──────┘└┘ └────
par └────┘ └─┘ ┴ ┴└──────┘└┘ └────
pid ┴ └─┘ ┴ └─────────┘ └──┘└
st ──────────────────────────────────────────────┘└───────┘└──────────────────
122 end
src ─────────┘
typ ─────────┘
doc ─────────┘
txt ─────────┘
par ─────────┘
pid ─────────┘
st ─────────┘└─┘└
123 ... = (∥f x∥ ⁻¹ * ∥f x∥) * (((r * ∥x₀∥)⁻¹) * ∥f x₀∥) * ∥x∥ : by ring
src └────
typ └────
doc └────
txt └────
par └────
pid └
st ────────────────────────────────────────────────────────────────────────┘└─────
124 ... = (((r * ∥x₀∥)⁻¹) * ∥f x₀∥) * ∥x∥ :
src ─────────┘
typ ─────────┘
doc ─────────┘
txt ─────────┘
par ─────────┘
pid ─────────┘
st ─────────┘└───────────────────────────────────────
125 by { rw [inv_mul_cancel, one_mul], simp [norm_eq_zero, hx] } } },
id └────────────┘ └─────┘ └──────────┘ └┘
src └──┘└────────────┘└┘└─────┘┴ └────┘└──────────┘└┘ └┘
typ └──┘└────────────┘└┘└─────┘┴ └────┘└──────────┘└┘└┘└┘
doc └──┘ └┘ ┴ └────┘ └┘ └┘
txt └──┘ └┘ ┴ └────┘ └┘ └┘
par └──┘ └┘ ┴ └────┘ └┘ └┘
pid └┘ └┘ ┴ ┴┴ └┘ ┴┴
st ─────────────┘└───────────────────┘└───────┘└─────────────────────────┘└────┘└
126 exact linear_map.continuous_of_bound f _ this }
id └────────────────────────────┘ ┴ └──┘
src └────┘└────────────────────────────┘┴ └─┘ ┴
typ └────┘└────────────────────────────┘┴┴└─┘└──┘┴
doc └────┘ ┴ └─┘ ┴
txt └────┘ ┴ └─┘ ┴
par └────┘ ┴ └─┘ ┴
pid ┴ ┴ └─┘ ┴
st ─────────────────────────────────────────────────┘└─
127 end
st ──┘
128
129 end normed_field
130
131 variables [nondiscrete_normed_field 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 F] [normed_space 𝕜 G]
id ┴└──────────────────────┘ └──────────┘ └──────────┘ └──────────┘
src └──────────────────────┘ └──────────┘ └──────────┘ └──────────┘
typ ┴└──────────────────────┘ └──────────┘ └──────────┘ └──────────┘
doc └──────────────────────┘ └──────────┘ └──────────┘ └──────────┘
132 (c : 𝕜) (f g : E →L[𝕜] F) (h : F →L[𝕜] G) (x y z : E)
id └─┘ ┴ └─┘ ┴
src └─┘ ┴ └─┘ ┴
typ └─┘ ┴ └─┘ ┴
doc └─┘ ┴ └─┘ ┴
133 include 𝕜
134
135 /-- A continuous linear map between normed spaces is bounded when the field is nondiscrete.
136 The continuity ensures boundedness on a ball of some radius `δ`. The nondiscreteness is then
137 used to rescale any element into an element of norm in `[δ/C, δ]`, whose image has a controlled norm.
138 The norm control for the original element follows by rescaling. -/
139 lemma linear_map.bound_of_continuous (f : E →ₗ[𝕜] F) (hf : continuous f) :
id ┴ └─┘┴┴ ┴ └────────┘ ┴
src └─┘ ┴ └────────┘
typ ┴ └─┘┴┴ ┴ └────────┘ ┴
doc └────────┘
140 ∃ C, 0 < C ∧ (∀ x : E, ∥f x∥ ≤ C * ∥x∥) :=
id ┴ ┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴ ┴┴┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴ ┴┴┴
141 begin
st └─────
142 have : continuous_at f 0 := continuous_iff_continuous_at.1 hf _,
id └───────────┘ ┴ └──────────────────────────┘ └┘
src └─────┘└───────────┘┴ └────┘└──────────────────────────┘└─┘ └┘
typ └─────┘└───────────┘┴┴└────┘└──────────────────────────┘└─┘└┘└┘
doc └─────┘└───────────┘┴ └────┘ └─┘ └┘
txt └─────┘ ┴ └────┘ └─┘ └┘
par └─────┘ ┴ └────┘ └─┘ └┘
pid └───┘└┘ ┴ ┴└───┘ └─┘ └┘
st ────────────────────────────────────────────────────────────────┘└─
143 rcases metric.tendsto_nhds_nhds.1 this 1 zero_lt_one with ⟨ε, ε_pos, hε⟩,
id └──────────────────────┘ └──┘ └─────────┘
src └─────┘└──────────────────────┘└─┘ └─┘└─────────┘└──────────────────┘
typ └─────┘└──────────────────────┘└─┘└──┘└─┘└─────────┘└──────────────────┘
doc └─────┘ └─┘ └─┘ └──────────────────┘
txt └─────┘ └─┘ └─┘ └──────────────────┘
par └─────┘ └─┘ └─┘ └──────────────────┘
pid ┴ └─┘ └─┘ └──────────────────┘
st ─────────────────────────────────────────────────────────────────────────┘└─
144 let δ := ε/2,
id ┴┴
src └───────┘ ┴┴
typ └───────┘┴┴┴
doc └───────┘ ┴
txt └───────┘ ┴
par └───────┘ ┴
pid └───┘┴└─┘ ┴
st ─────────────┘└─
145 have δ_pos : δ > 0 := half_pos ε_pos,
id ┴ ┴ └──────┘ └───┘
src └───────────┘ ┴┴└────┘└──────┘┴
typ └───────────┘┴┴┴└────┘└──────┘┴└───┘
doc └───────────┘ ┴ └────┘ ┴
txt └───────────┘ ┴ └────┘ ┴
par └───────────┘ ┴ └────┘ ┴
pid └────────┘└─┘ ┴ ┴└───┘ ┴
st ─────────────────────────────────────┘└─
146 have H : ∀{a}, ∥a∥ ≤ δ → ∥f a∥ ≤ 1,
id ┴ ┴ ┴ ┴ ┴
src └───────┘ └─┘ ┴┴ ┴┴┴┴ ┴ ┴ ┴ ┴ └┘
typ └───────┘ └─┘ ┴┴ ┴┴┴┴┴┴ ┴ ┴┴ ┴ └┘
doc └───────┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘
txt └───────┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘
par └───────┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘
pid └────┘└─┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴
st ───────────────────────────────────┘└─
147 { assume a ha,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └─────────┘
st ───┘└─────────┘└─
148 have : dist (f a) (f 0) ≤ 1,
id └──┘ ┴ ┴
src └─────┘└──┘┴ ┴ └┘ └──┘ └┘
typ └─────┘└──┘┴ ┴┴└┘ ┴└──┘ └┘
doc └─────┘ ┴ ┴ └┘ └──┘ └┘
txt └─────┘ ┴ ┴ └┘ └──┘ └┘
par └─────┘ ┴ ┴ └┘ └──┘ └┘
pid └───┘└┘ ┴ ┴ └┘ └──┘ ┴┴
st ──────────────────────────────┘└─
149 { apply le_of_lt (hε _),
id └──────┘ └┘
src └────┘└──────┘┴ └─┘
typ └────┘└──────┘┴ └┘└─┘
doc └────┘ ┴ └─┘
txt └────┘ ┴ └─┘
par └────┘ ┴ └─┘
pid ┴ ┴ └─┘
st ─────┘└───────────────────┘└─
150 rw [dist_eq_norm, sub_zero],
id └──────────┘ └──────┘
src └──┘└──────────┘└┘└──────┘┴
typ └──┘└──────────┘└┘└──────┘┴
doc └──┘ └┘ ┴
txt └──┘ └┘ ┴
par └──┘ └┘ ┴
pid └┘ └┘ ┴
st ─────────────────────┘└────────┘└──
151 exact lt_of_le_of_lt ha (half_lt_self ε_pos) },
id └────────────┘ └┘ └──────────┘ └───┘
src └────┘└────────────┘┴ ┴ └──────────┘┴ └┘
typ └────┘└────────────┘┴└┘┴ └──────────┘┴└───┘└┘
doc └────┘ ┴ ┴ ┴ └┘
txt └────┘ ┴ ┴ ┴ └┘
par └────┘ ┴ ┴ ┴ └┘
pid ┴ ┴ ┴ ┴ ┴┴
st ──────────────────────────────────────────────────┘└┘└
152 simpa using this },
id └──┘
src └──────────┘ ┴
typ └──────────┘└──┘┴
doc └──────────┘ ┴
txt └──────────┘ ┴
par └──────────┘ ┴
pid ┴└────┘ ┴
st ────────────────────┘└┘└
153 rcases normed_field.exists_one_lt_norm 𝕜 with ⟨c, hc⟩,
id └─────────────────────────────┘ ┴
src └─────┘└─────────────────────────────┘┴ └───────────┘
typ └─────┘└─────────────────────────────┘┴┴└───────────┘
doc └─────┘ ┴ └───────────┘
txt └─────┘ ┴ └───────────┘
par └─────┘ ┴ └───────────┘
pid ┴ ┴ └───────────┘
st ──────────────────────────────────────────────────────┘└─
154 refine ⟨δ⁻¹ * ∥c∥, mul_pos (inv_pos δ_pos) (lt_trans zero_lt_one hc), (λx, _)⟩,
id ┴└┘ ┴ ┴ └─────┘ └─────┘ └───┘ └──────┘ └─────────┘ └┘
src └─────┘ └┘┴┴┴ └┘└─────┘┴ └─────┘┴ └┘ └──────┘┴└─────────┘┴ └─┘ └────┘
typ └─────┘ ┴└┘┴┴┴ ┴ └┘└─────┘┴ └─────┘┴└───┘└┘ └──────┘┴└─────────┘┴└┘└─┘ └────┘
doc └─────┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └─┘ └────┘
txt └─────┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └─┘ └────┘
par └─────┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └─┘ └────┘
pid ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └─┘ └────┘
st ───────────────────────────────────────────────────────────────────────────────┘└─
155 by_cases h : x = 0,
id ┴ ┴
src └───────┘ └─┘ ┴┴└┘
typ └───────┘ └─┘┴┴┴└┘
doc └───────┘ └─┘ ┴ └┘
txt └───────┘ └─┘ ┴ └┘
par └───────┘ └─┘ ┴ └┘
pid ┴ └─┘ ┴ ┴┴
st ───────────────────┘└─
156 { simp only [h, norm_zero, mul_zero, linear_map.map_zero] },
id ┴ └───────┘ └──────┘ └─────────────────┘
src └─────────┘ └┘└───────┘└┘└──────┘└┘└─────────────────┘└┘
typ └─────────┘┴└┘└───────┘└┘└──────┘└┘└─────────────────┘└┘
doc └─────────┘ └┘ └┘ └┘ └┘
txt └─────────┘ └┘ └┘ └┘ └┘
par └─────────┘ └┘ └┘ └┘ └┘
pid ┴└──┘└┘ └┘ └┘ └┘ ┴┴
st ───┘└──────────────────────────────────────────────────────┘└┘└
157 { rcases rescale_to_shell hc δ_pos h with ⟨d, hd, dxle, ledx, dinv⟩,
id └──────────────┘ └┘ └───┘ ┴
src └─────┘└──────────────┘┴ ┴ ┴ └─────────────────────────────┘
typ └─────┘└──────────────┘┴└┘┴└───┘┴┴└─────────────────────────────┘
doc └─────┘└──────────────┘┴ ┴ ┴ └─────────────────────────────┘
txt └─────┘ ┴ ┴ ┴ └─────────────────────────────┘
par └─────┘ ┴ ┴ ┴ └─────────────────────────────┘
pid ┴ ┴ ┴ ┴ └─────────────────────────────┘
st ────────────────────────────────────────────────────────────────────┘└─
158 calc ∥f x∥
id └──┘
src └──┘
typ └──┘
doc └──┘
st ───────────────
159 = ∥f ((d⁻¹ * d) • x)∥ : by rwa [inv_mul_cancel, one_smul]
id ┴ ┴ ┴ └────────────┘ └──────┘
src └───┘└────────────┘└┘└──────┘└─
typ ┴ ┴ ┴ └───┘└────────────┘└┘└──────┘└─
doc └───┘ └┘ └─
txt └───┘ └┘ └─
par └───┘ └┘ └─
pid └┘ └┘ ┴└
st ───────────────────────────────┘└──────────────────┘└────────┘┴└
160 ... = ∥d∥⁻¹ * ∥f (d • x)∥ :
id ┴
src ─────┘ ┴
typ ─────┘ ┴
doc ─────┘
txt ─────┘
par ─────┘
pid ─────┘
st ─────┘└───────────────────────────
161 by rw [mul_smul, linear_map.map_smul, norm_smul, normed_field.norm_inv]
id └──────┘ └─────────────────┘ └───────┘ └───────────────────┘
src └──┘└──────┘└┘└─────────────────┘└┘└───────┘└┘└───────────────────┘└─
typ └──┘└──────┘└┘└─────────────────┘└┘└───────┘└┘└───────────────────┘└─
doc └──┘ └┘ └┘ └┘ └─
txt └──┘ └┘ └┘ └┘ └─
par └──┘ └┘ └┘ └┘ └─
pid └┘ └┘ └┘ └┘ ┴└
st ─────────┘└───────────┘└───────────────────┘└─────────┘└─────────────────────┘┴└
162 ... ≤ ∥d∥⁻¹ * 1 :
src ─────┘
typ ─────┘
doc ─────┘
txt ─────┘
par ─────┘
pid ─────┘
st ─────┘└─────────────────
163 mul_le_mul_of_nonneg_left (H dxle) (by { rw ← normed_field.norm_inv, exact norm_nonneg _ })
id └───────────────────────┘ ┴ └──┘ └───────────────────┘ └─────────┘
src └───────────────────────┘ └───┘└───────────────────┘ └────┘└─────────┘└─┘
typ └───────────────────────┘ ┴ └──┘ └───┘└───────────────────┘ └────┘└─────────┘└─┘
doc └───┘ └────┘ └─┘
txt └───┘ └────┘ └─┘
par └───┘ └────┘ └─┘
pid └─┘ ┴ └┘┴
st ─────────────────────────────────────────────┘└───────────────────────────┘└────────────────────┘└┘└
164 ... ≤ δ⁻¹ * ∥c∥ * ∥x∥ : by { rw mul_one, exact dinv } }
id ┴ ┴ └─────┘ └──┘
src └─┘└─────┘ └────┘ ┴
typ ┴ ┴ └─┘└─────┘ └────┘└──┘┴
doc └─┘ └────┘ ┴
txt └─┘ └────┘ ┴
par └─┘ └────┘ ┴
pid ┴ ┴ ┴
st ───────────────────────────────┘└───────────┘└───────────┘└───
165 end
st ──┘
166
167 namespace continuous_linear_map
168
169 theorem bound : ∃ C, 0 < C ∧ (∀ x : E, ∥f x∥ ≤ C * ∥x∥) :=
id ┴ ┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴ ┴┴┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴ ┴┴┴
170 f.to_linear_map.bound_of_continuous f.2
id ┴└────────────┘└──────────────────┘ ┴┴
src └────────────┘└──────────────────┘ ┴
typ ┴└────────────┘└──────────────────┘ ┴┴
doc └──────────────────┘
171
172 section
173 open asymptotics filter
174
175 theorem is_O_id (l : filter E) : is_O f (λ x, x) l :=
id └────┘ ┴ └──┘ ┴ ┴ ┴ ┴
src └────┘ └──┘
typ └────┘ ┴ └──┘ ┴ ┴ ┴ ┴
doc └──┘
176 let ⟨M, hMp, hM⟩ := f.bound in is_O_of_le' l hM
id └─┘ └┘ ┴└────┘ └─────────┘ ┴
src └────┘ └─────────┘
typ └─┘ └┘ ┴└────┘ └─────────┘ ┴
177
178 theorem is_O_comp {E : Type*} (g : F →L[𝕜] G) (f : E → F) (l : filter E) :
id ┴ └─┘┴┴ ┴ ┴ ┴ └────┘ ┴
src └─┘ ┴ └────┘
typ ┴ └─┘┴┴ ┴ ┴ ┴ └────┘ ┴
doc └─┘ ┴
179 is_O (λ x', g (f x')) f l :=
id └──┘ └┘ ┴ ┴ └┘ ┴ ┴
src └──┘
typ └──┘ └┘ ┴ ┴ └┘ ┴ ┴
doc └──┘
180 (g.is_O_id ⊤).comp_tendsto lattice.le_top
id ┴└──────┘ ┴ └──────────┘ └────────────┘
src └──────┘ ┴ └──────────┘ └────────────┘
typ ┴└──────┘ ┴ └──────────┘ └────────────┘
181
182 theorem is_O_sub (f : E →L[𝕜] F) (l : filter E) (x : E) :
id ┴ └─┘┴┴ ┴ └────┘ ┴ ┴
src └─┘ ┴ └────┘
typ ┴ └─┘┴┴ ┴ └────┘ ┴ ┴
doc └─┘ ┴
183 is_O (λ x', f (x' - x)) (λ x', x' - x) l :=
id └──┘ └┘ ┴ └┘ ┴ ┴ └┘ └┘ ┴ ┴ ┴
src └──┘ ┴ ┴
typ └──┘ └┘ ┴ └┘ ┴ ┴ └┘ └┘ ┴ ┴ ┴
doc └──┘
184 f.is_O_comp _ l
id ┴└────────┘ ┴
src └────────┘
typ ┴└────────┘ ┴
185
186 end
187
188 section op_norm
189 open set real
190
191 set_option class.instance_max_depth 100
doc └──────────────────────┘
192
193 /-- The operator norm of a continuous linear map is the inf of all its bounds. -/
194 def op_norm := Inf { c | c ≥ 0 ∧ ∀ x, ∥f x∥ ≤ c * ∥x∥ }
id └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴ ┴┴┴
src └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴ ┴┴┴
195 instance has_op_norm : has_norm (E →L[𝕜] F) := ⟨op_norm⟩
id └──────┘ ┴ └─┘┴┴ ┴ └─────┘
src └──────┘ └─┘ ┴ └─────┘
typ └──────┘ ┴ └─┘┴┴ ┴ └─────┘
doc └──────┘ └─┘ ┴ └─────┘
196
197 -- So that invocations of `real.Inf_le` make sense: we show that the set of
198 -- bounds is nonempty and bounded below.
199 lemma bounds_nonempty {f : E →L[𝕜] F} :
id ┴ └─┘┴┴ ┴
src └─┘ ┴
typ ┴ └─┘┴┴ ┴
doc └─┘ ┴
200 ∃ c, c ∈ { c | 0 ≤ c ∧ ∀ x, ∥f x∥ ≤ c * ∥x∥ } :=
id ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴ ┴┴┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴ ┴┴┴
201 let ⟨M, hMp, hMb⟩ := f.bound in ⟨M, le_of_lt hMp, hMb⟩
id └─┘ ┴ └─┘ └─┘ ┴└────┘ └──────┘
src └────┘ └──────┘
typ └─┘ ┴ └─┘ └─┘ ┴└────┘ └──────┘
202
203 lemma bounds_bdd_below {f : E →L[𝕜] F} :
id ┴ └─┘┴┴ ┴
src └─┘ ┴
typ ┴ └─┘┴┴ ┴
doc └─┘ ┴
204 bdd_below { c | 0 ≤ c ∧ ∀ x, ∥f x∥ ≤ c * ∥x∥ } :=
id └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴ ┴┴┴
src └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴ ┴┴┴
doc └───────┘
205 ⟨0, λ _ ⟨hn, _⟩, hn⟩
id ┴ ┴└┘
typ ┴ ┴└┘
206
207 lemma op_norm_nonneg : 0 ≤ ∥f∥ :=
id ┴ ┴┴┴
src ┴ ┴ ┴
typ ┴ ┴┴┴
208 lb_le_Inf _ bounds_nonempty (λ _ ⟨hx, _⟩, hx)
id └───────┘ └─────────────┘ ┴ ┴└┘
src └───────┘ └─────────────┘
typ └───────┘ └─────────────┘ ┴ ┴└┘
209
210 /-- The fundamental property of the operator norm: `∥f x∥ ≤ ∥f∥ * ∥x∥`. -/
211 theorem le_op_norm : ∥f x∥ ≤ ∥f∥ * ∥x∥ :=
id ┴┴ ┴┴ ┴ ┴┴┴ ┴ ┴┴┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴┴ ┴┴ ┴ ┴┴┴ ┴ ┴┴┴
212 classical.by_cases
id └────────────────┘
src └────────────────┘
typ └────────────────┘
213 (λ heq : x = 0, by { rw heq, simp })
id ┴ ┴ └─┘
src ┴ └─┘└─┘ └───┘
typ ┴ ┴ └─┘└─┘ └───┘
doc └─┘ └───┘
txt └─┘ └───┘
par └─┘ └───┘
pid ┴ ┴
st └───────┘└─────┘└┘
214 (λ hne, have hlt : 0 < ∥x∥, from (norm_pos_iff _).2 hne,
id └─┘ ┴ ┴┴┴ └──────────┘ ┴ └─┘
src ┴ ┴ ┴ └──────────┘ ┴
typ └─┘ ┴ ┴┴┴ └──────────┘ ┴ └─┘
215 le_mul_of_div_le hlt ((le_Inf _ bounds_nonempty bounds_bdd_below).2
id └──────────────┘ └─┘ └────┘ └─────────────┘ └──────────────┘ ┴
src └──────────────┘ └────┘ └─────────────┘ └──────────────┘ ┴
typ └──────────────┘ └─┘ └────┘ └─────────────┘ └──────────────┘ ┴
216 (λ c ⟨_, hc⟩, div_le_of_le_mul hlt (by { rw mul_comm, apply hc }))))
id ┴ ┴ └──────────────┘ └─┘ └──────┘
src └──────────────┘ └─┘└──────┘ └────┘ ┴
typ ┴ ┴ └──────────────┘ └─┘ └─┘└──────┘ └────┘ ┴
doc └─┘ └────┘ ┴
txt └─┘ └────┘ ┴
par └─┘ └────┘ ┴
pid ┴ ┴ ┴
st └────────────┘└─────────┘└┘
217
218 lemma ratio_le_op_norm : ∥f x∥ / ∥x∥ ≤ ∥f∥ :=
id ┴┴ ┴┴ ┴ ┴┴┴ ┴ ┴┴┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴┴ ┴┴ ┴ ┴┴┴ ┴ ┴┴┴
219 (or.elim (lt_or_eq_of_le (norm_nonneg _))
id └─────┘ └────────────┘ └─────────┘
src └─────┘ └────────────┘ └─────────┘
typ └─────┘ └────────────┘ └─────────┘
220 (λ hlt, div_le_of_le_mul hlt (by { rw mul_comm, apply le_op_norm }))
id └─┘ └──────────────┘ └─┘ └──────┘ └────────┘
src └──────────────┘ └─┘└──────┘ └────┘└────────┘┴
typ └─┘ └──────────────┘ └─┘ └─┘└──────┘ └────┘└────────┘┴
doc └─┘ └────┘└────────┘┴
txt └─┘ └────┘ ┴
par └─┘ └────┘ ┴
pid ┴ ┴ ┴
st └────────────┘└─────────────────┘└┘
221 (λ heq, by { rw [←heq, div_zero], apply op_norm_nonneg }))
id └─┘ └─┘ └──────┘ └────────────┘
src └─┘ └───┘└─┘└┘└──────┘┴ └────┘└────────────┘┴
typ └─┘ └───┘└─┘└┘└──────┘┴ └────┘└────────────┘┴
doc └───┘ └┘ ┴ └────┘ ┴
txt └───┘ └┘ ┴ └────┘ ┴
par └───┘ └┘ ┴ └────┘ ┴
pid └─┘ └┘ ┴ ┴ ┴
st └─────────┘└────────┘└──────────────────────┘└┘
222
223 /-- The image of the unit ball under a continuous linear map is bounded. -/
224 lemma unit_le_op_norm : ∥x∥ ≤ 1 → ∥f x∥ ≤ ∥f∥ :=
id ┴┴┴ ┴ ┴┴ ┴┴ ┴ ┴┴┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴┴┴ ┴ ┴┴ ┴┴ ┴ ┴┴┴
225 λ hx, begin
id └┘
typ └┘
st └─────
226 rw [←(mul_one ∥f∥)],
id └─────┘ ┴┴┴
src └───┘ └─────┘┴┴ ┴└┘
typ └───┘ └─────┘┴┴┴┴└┘
doc └───┘ ┴ └┘
txt └───┘ ┴ └┘
par └───┘ ┴ └┘
pid └─┘ ┴ └┘
st ───────────────────┘└──
227 calc _ ≤ ∥f∥ * ∥x∥ : le_op_norm _ _
id └──┘ ┴ ┴ ┴ └────────┘
src └──┘ ┴ └────────┘
typ └──┘ ┴ ┴ ┴ └────────┘
doc └──┘ └────────┘
st ──────────────────────────────────────
228 ... ≤ _ : mul_le_mul_of_nonneg_left hx (op_norm_nonneg _)
id └───────────────────────┘ └┘ └────────────┘
src └───────────────────────┘ └────────────┘
typ └───────────────────────┘ └┘ └────────────┘
st ─────────────────────────────────────────────────────────────┘└
229 end
st ──┘
230
231 /-- If one controls the norm of every `A x`, then one controls the norm of `A`. -/
232 lemma op_norm_le_bound {M : ℝ} (hMp: 0 ≤ M) (hM : ∀ x, ∥f x∥ ≤ M * ∥x∥) :
id ┴ ┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴ ┴┴┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴ ┴┴┴
233 ∥f∥ ≤ M :=
id ┴┴┴ ┴ ┴
src ┴ ┴ ┴
typ ┴┴┴ ┴ ┴
234 Inf_le _ bounds_bdd_below ⟨hMp, hM⟩
id └────┘ └──────────────┘ └─┘ └┘
src └────┘ └──────────────┘
typ └────┘ └──────────────┘ └─┘ └┘
235
236 /-- The operator norm satisfies the triangle inequality. -/
237 theorem op_norm_add_le : ∥f + g∥ ≤ ∥f∥ + ∥g∥ :=
id ┴┴ ┴ ┴┴ ┴ ┴┴┴ ┴ ┴┴┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴┴ ┴ ┴┴ ┴ ┴┴┴ ┴ ┴┴┴
238 Inf_le _ bounds_bdd_below
id └────┘ └──────────────┘
src └────┘ └──────────────┘
typ └────┘ └──────────────┘
239 ⟨add_nonneg (op_norm_nonneg _) (op_norm_nonneg _), λ x, by { rw add_mul,
id └────────┘ └────────────┘ └────────────┘ ┴ └─────┘
src └────────┘ └────────────┘ └────────────┘ └─┘└─────┘
typ └────────┘ └────────────┘ └────────────┘ ┴ └─┘└─────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st └───────────┘└─
240 exact norm_add_le_of_le (le_op_norm _ _) (le_op_norm _ _) }⟩
id └───────────────┘ └────────┘
src └────┘└───────────────┘┴ └────┘ └────────┘└────┘
typ └────┘└───────────────┘┴ └────┘ └────────┘└────┘
doc └────┘ ┴ └────┘ └────────┘└────┘
txt └────┘ ┴ └────┘ └────┘
par └────┘ ┴ └────┘ └────┘
pid ┴ ┴ └────┘ └───┘┴
st ─────────────────────────────────────────────────────────────┘└┘
241
242 /-- An operator is zero iff its norm vanishes. -/
243 theorem op_norm_zero_iff : ∥f∥ = 0 ↔ f = 0 :=
id ┴┴┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴┴┴ ┴ ┴ ┴ ┴
244 iff.intro
id └───────┘
src └───────┘
typ └───────┘
245 (λ hn, continuous_linear_map.ext (λ x, (norm_le_zero_iff _).1
id └┘ └───────────────────────┘ ┴ └──────────────┘ ┴
src └───────────────────────┘ └──────────────┘ ┴
typ └┘ └───────────────────────┘ ┴ └──────────────┘ ┴
246 (calc _ ≤ ∥f∥ * ∥x∥ : le_op_norm _ _
id ┴┴┴ ┴ ┴┴┴ └────────┘
src ┴ ┴ ┴ ┴ ┴ └────────┘
typ ┴┴┴ ┴ ┴┴┴ └────────┘
doc └────────┘
247 ... = _ : by rw [hn, zero_mul])))
id └┘ └──────┘
src └──┘ └┘└──────┘┴
typ └──┘└┘└┘└──────┘┴
doc └──┘ └┘ ┴
txt └──┘ └┘ ┴
par └──┘ └┘ ┴
pid └┘ └┘ ┴
st └─────┘└────────┘┴
248 (λ hf, le_antisymm (Inf_le _ bounds_bdd_below
id └┘ └─────────┘ └────┘ └──────────────┘
src └─────────┘ └────┘ └──────────────┘
typ └┘ └─────────┘ └────┘ └──────────────┘
249 ⟨ge_of_eq rfl, λ _, le_of_eq (by { rw [zero_mul, hf], exact norm_zero })⟩)
id └──────┘ └─┘ ┴ └──────┘ └──────┘ └┘ └───────┘
src └──────┘ └─┘ └──────┘ └──┘└──────┘└┘ ┴ └────┘└───────┘┴
typ └──────┘ └─┘ ┴ └──────┘ └──┘└──────┘└┘└┘┴ └────┘└───────┘┴
doc └──┘ └┘ ┴ └────┘ ┴
txt └──┘ └┘ ┴ └────┘ ┴
par └──┘ └┘ ┴ └────┘ ┴
pid └┘ └┘ ┴ ┴ ┴
st └─────────────┘└──┘└─────────────────┘└┘
250 (op_norm_nonneg _))
id └────────────┘
src └────────────┘
typ └────────────┘
251
252 @[simp] lemma norm_zero : ∥(0 : E →L[𝕜] F)∥ = 0 :=
id ┴ ┴ └─┘┴┴ ┴ ┴ ┴
src ┴ └─┘ ┴ ┴ ┴
typ ┴ ┴ └─┘┴┴ ┴ ┴ ┴
doc └──┘ └─┘ ┴
253 by rw op_norm_zero_iff
id └──────────────┘
src └─┘└──────────────┘└
typ └─┘└──────────────┘└
doc └─┘└──────────────┘└
txt └─┘ └
par └─┘ └
pid ┴ └
st └────────────────────
254
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
255 /-- The norm of the identity is at most `1`. It is in fact `1`, except when the space is trivial
256 where it is `0`. It means that one can not do better than an inequality in general. -/
257 lemma norm_id : ∥(id : E →L[𝕜] E)∥ ≤ 1 :=
id ┴ └┘ ┴ └─┘┴┴ ┴ ┴ ┴
src ┴ └┘ └─┘ ┴ ┴ ┴
typ ┴ └┘ ┴ └─┘┴┴ ┴ ┴ ┴
doc └┘ └─┘ ┴
258 op_norm_le_bound _ zero_le_one (λx, by simp)
id └──────────────┘ └─────────┘ ┴
src └──────────────┘ └─────────┘ └──┘
typ └──────────────┘ └─────────┘ ┴ └──┘
doc └──────────────┘ └──┘
txt └──┘
par └──┘
st └───┘
259
260 /-- The operator norm is homogeneous. -/
261 lemma op_norm_smul : ∥c • f∥ = ∥c∥ * ∥f∥ :=
id ┴┴ ┴ ┴┴ ┴ ┴┴┴ ┴ ┴┴┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴┴ ┴ ┴┴ ┴ ┴┴┴ ┴ ┴┴┴
262 le_antisymm
id └─────────┘
src └─────────┘
typ └─────────┘
263 (Inf_le _ bounds_bdd_below
id └────┘ └──────────────┘
src └────┘ └──────────────┘
typ └────┘ └──────────────┘
264 ⟨mul_nonneg (norm_nonneg _) (op_norm_nonneg _), λ _,
id └────────┘ └─────────┘ └────────────┘ ┴
src └────────┘ └─────────┘ └────────────┘
typ └────────┘ └─────────┘ └────────────┘ ┴
265 begin
st └─────
266 erw [norm_smul, mul_assoc],
id └───────┘ └───────┘
src └───┘└───────┘└┘└───────┘┴
typ └───┘└───────┘└┘└───────┘┴
doc └───┘ └┘ ┴
txt └───┘ └┘ ┴
par └───┘ └┘ ┴
pid └┘ └┘ ┴
st ───────────────────┘└─────────┘└──
267 exact mul_le_mul_of_nonneg_left (le_op_norm _ _) (norm_nonneg _)
id └───────────────────────┘ └────────┘ └─────────┘
src └────┘└───────────────────────┘┴ └────────┘└────┘ └─────────┘└───
typ └────┘└───────────────────────┘┴ └────────┘└────┘ └─────────┘└───
doc └────┘ ┴ └────────┘└────┘ └───
txt └────┘ ┴ └────┘ └───
par └────┘ ┴ └────┘ └───
pid ┴ ┴ └────┘ └─┘└
st ───────────────────────────────────────────────────────────────────────
268 end⟩)
src ───┘
typ ───┘
doc ───┘
txt ───┘
par ───┘
pid ───┘
st ───┘└─┘
269 (lb_le_Inf _ bounds_nonempty (λ _ ⟨hn, hc⟩,
id └───────┘ └─────────────┘ ┴ ┴
src └───────┘ └─────────────┘
typ └───────┘ └─────────────┘ ┴ ┴
270 (or.elim (lt_or_eq_of_le (norm_nonneg c))
id └─────┘ └────────────┘ └─────────┘ ┴
src └─────┘ └────────────┘ └─────────┘
typ └─────┘ └────────────┘ └─────────┘ ┴
271 (λ hlt,
id └─┘
typ └─┘
272 begin
st └─────
273 rw mul_comm,
id └──────┘
src └─┘└──────┘
typ └─┘└──────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ────────────────────┘└─
274 exact mul_le_of_le_div hlt (Inf_le _ bounds_bdd_below
id └──────────────┘ └────┘ └──────────────┘
src └────┘└──────────────┘┴ ┴ └────┘└─┘└──────────────┘└
typ └────┘└──────────────┘┴ ┴ └────┘└─┘└──────────────┘└
doc └────┘ ┴ ┴ └─┘ └
txt └────┘ ┴ ┴ └─┘ └
par └────┘ ┴ ┴ └─┘ └
pid ┴ ┴ ┴ └─┘ └
st ────────────────────────────────────────────────────────────────
275 ⟨div_nonneg hn hlt, λ _,
id └────────┘ └┘ └─┘
src ─────────┘ └────────┘┴ ┴ └┘ └───
typ ─────────┘ └────────┘┴└┘┴└─┘└┘ └───
doc ─────────┘ ┴ ┴ └┘ └───
txt ─────────┘ ┴ ┴ └┘ └───
par ─────────┘ ┴ ┴ └┘ └───
pid ─────────┘ ┴ ┴ └┘ └───
st ───────────────────────────────────
276 (by { rw div_mul_eq_mul_div, exact le_div_of_mul_le hlt
id └────────────────┘ └──────────────┘ └─┘
src ─────────┘ └─┘└─┘└────────────────┘└──────┘└──────────────┘┴ └
typ ─────────┘ └─┘└─┘└────────────────┘└──────┘└──────────────┘┴└─┘└
doc ─────────┘ └─┘└─┘ └──────┘ ┴ └
txt ─────────┘ └─┘└─┘ └──────┘ ┴ └
par ─────────┘ └─┘└─┘ └──────┘ ┴ └
pid ─────────┘ └────┘ └──────┘ ┴ └
st ────────────┘└──────────────────────┘└────────────────────────────
277 (by { rw [ mul_comm, ←norm_smul ], exact hc _ }) })⟩)
id └──────┘ └───────┘ └┘
src ─────────┘ └─┘└───┘└──────┘└─┘└───────┘└┘└──────┘ └──────────
typ ─────────┘ └─┘└───┘└──────┘└─┘└───────┘└┘└──────┘└┘└──────────
doc ─────────┘ └─┘└───┘ └─┘ └┘└──────┘ └──────────
txt ─────────┘ └─┘└───┘ └─┘ └┘└──────┘ └──────────
par ─────────┘ └─┘└───┘ └─┘ └┘└──────┘ └──────────
pid ─────────┘ └──────┘ └─┘ └────────┘ └────────┘└
st ────────────┘└──────────────┘└──────────┘└─────────────┘┴└┘┴└───
278 end)
src ───────┘
typ ───────┘
doc ───────┘
txt ───────┘
par ───────┘
pid ───────┘
st ───────┘└─┘
279 (λ heq, by { rw [←heq, zero_mul], exact hn }))))
id └─┘ └─┘ └──────┘ └┘
src └─┘ └───┘└─┘└┘└──────┘┴ └────┘ ┴
typ └─┘ └───┘└─┘└┘└──────┘┴ └────┘└┘┴
doc └───┘ └┘ ┴ └────┘ ┴
txt └───┘ └┘ ┴ └────┘ ┴
par └───┘ └┘ ┴ └────┘ ┴
pid └─┘ └┘ ┴ ┴ ┴
st └─────────┘└────────┘└──────────┘└┘
280
281 lemma op_norm_neg : ∥-f∥ = ∥f∥ := calc
id ┴┴┴┴ ┴ ┴┴┴
src ┴┴ ┴ ┴ ┴ ┴
typ ┴┴┴┴ ┴ ┴┴┴
282 ∥-f∥ = ∥(-1:𝕜) • f∥ : by rw neg_one_smul
id ┴┴┴┴ ┴ ┴ ┴ ┴ ┴┴ └──────────┘
src ┴┴ ┴ ┴ ┴ ┴ ┴ └─┘└──────────┘└
typ ┴┴┴┴ ┴ ┴ ┴ ┴ ┴┴ └─┘└──────────┘└
doc └─┘ └
txt └─┘ └
par └─┘ └
pid ┴ └
st └────────────────
283 ... = ∥(-1:𝕜)∥ * ∥f∥ : by rw op_norm_smul
id ┴ ┴ ┴ ┴ ┴ ┴┴┴ └──────────┘
src ─┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘└──────────┘└
typ ─┘ ┴ ┴ ┴ ┴ ┴ ┴┴┴ └─┘└──────────┘└
doc ─┘ └─┘└──────────┘└
txt ─┘ └─┘ └
par ─┘ └─┘ └
pid ─┘ ┴ └
st ─┘ └────────────────
284 ... = ∥f∥ : by simp
id ┴┴┴
src ─┘ ┴ ┴ └────
typ ─┘ ┴┴┴ └────
doc ─┘ └────
txt ─┘ └────
par ─┘ └────
pid ─┘ └
st ─┘ └─────
285
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
286 /-- Continuous linear maps themselves form a normed space with respect to
287 the operator norm. -/
288 instance to_normed_group : normed_group (E →L[𝕜] F) :=
id └──────────┘ ┴ └─┘┴┴ ┴
src └──────────┘ └─┘ ┴
typ └──────────┘ ┴ └─┘┴┴ ┴
doc └──────────┘ └─┘ ┴
289 normed_group.of_core _ ⟨op_norm_zero_iff, op_norm_add_le, op_norm_neg⟩
id └──────────────────┘ └──────────────┘ └────────────┘ └─────────┘
src └──────────────────┘ └──────────────┘ └────────────┘ └─────────┘
typ └──────────────────┘ └──────────────┘ └────────────┘ └─────────┘
doc └──────────────────┘ └──────────────┘ └────────────┘
290
291 instance to_normed_space : normed_space 𝕜 (E →L[𝕜] F) :=
id └──────────┘ ┴ ┴ └─┘┴┴ ┴
src └──────────┘ └─┘ ┴
typ └──────────┘ ┴ ┴ └─┘┴┴ ┴
doc └──────────┘ └─┘ ┴
292 ⟨op_norm_smul⟩
id └──────────┘
src └──────────┘
typ └──────────┘
doc └──────────┘
293
294 /-- The operator norm is submultiplicative. -/
295 lemma op_norm_comp_le : ∥comp h f∥ ≤ ∥h∥ * ∥f∥ :=
id ┴└──┘ ┴ ┴┴ ┴ ┴┴┴ ┴ ┴┴┴
src ┴└──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴└──┘ ┴ ┴┴ ┴ ┴┴┴ ┴ ┴┴┴
doc └──┘
296 (Inf_le _ bounds_bdd_below
id └────┘ └──────────────┘
src └────┘ └──────────────┘
typ └────┘ └──────────────┘
297 ⟨mul_nonneg (op_norm_nonneg _) (op_norm_nonneg _), λ x,
id └────────┘ └────────────┘ └────────────┘ ┴
src └────────┘ └────────────┘ └────────────┘
typ └────────┘ └────────────┘ └────────────┘ ┴
298 begin
st └─────
299 rw mul_assoc,
id └───────┘
src └─┘└───────┘
typ └─┘└───────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ───────────────┘└─
300 calc _ ≤ ∥h∥ * ∥f x∥: le_op_norm _ _
id └──┘ ┴┴┴ ┴ ┴ ┴
src └──┘ ┴ ┴ ┴
typ └──┘ ┴┴┴ ┴ ┴ ┴
doc └──┘
st ─────────────────────────────────────────
301 ... ≤ _ : mul_le_mul_of_nonneg_left
id └───────────────────────┘
src └───────────────────────┘
typ └───────────────────────┘
st ────────────────────────────────────────
302 (le_op_norm _ _) (op_norm_nonneg _)
id └────────┘ └────────────┘
src └────────┘ └────────────┘
typ └────────┘ └────────────┘
doc └────────┘
st ────────────────────────────────────────────────┘└
303 end⟩)
st ────┘
304
305 /-- continuous linear maps are Lipschitz continuous. -/
306 theorem lipschitz : lipschitz_with ⟨∥f∥, op_norm_nonneg f⟩ f :=
id └────────────┘ ┴┴┴ └────────────┘ ┴ ┴
src └────────────┘ ┴ ┴ └────────────┘
typ └────────────┘ ┴┴┴ └────────────┘ ┴ ┴
doc └────────────┘
307 λ x y, by { rw [dist_eq_norm, dist_eq_norm, ←map_sub], apply le_op_norm }
id ┴ ┴ └──────────┘ └──────────┘ └─────┘ └────────┘
src └──┘└──────────┘└┘└──────────┘└─┘└─────┘┴ └────┘└────────┘┴
typ ┴ ┴ └──┘└──────────┘└┘└──────────┘└─┘└─────┘┴ └────┘└────────┘┴
doc └──┘ └┘ └─┘ ┴ └────┘└────────┘┴
txt └──┘ └┘ └─┘ ┴ └────┘ ┴
par └──┘ └┘ └─┘ ┴ └────┘ ┴
pid └┘ └┘ └─┘ ┴ ┴ ┴
st └─────────────────┘└────────────┘└────────┘└──────────────────┘└┘
308
309 /-- A continuous linear map is automatically uniformly continuous. -/
310 protected theorem uniform_continuous : uniform_continuous f :=
id └────────────────┘ ┴
src └────────────────┘
typ └────────────────┘ ┴
311 f.lipschitz.to_uniform_continuous
id ┴└────────┘└────────────────────┘
src └────────┘└────────────────────┘
typ ┴└────────┘└────────────────────┘
doc └────────┘└────────────────────┘
312
313 variable {f}
314 /-- A continuous linear map is an isometry if and only if it preserves the norm. -/
315 lemma isometry_iff_norm_image_eq_norm :
316 isometry f ↔ ∀x, ∥f x∥ = ∥x∥ :=
id └──────┘ ┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴┴┴
src └──────┘ ┴ ┴ ┴ ┴ ┴ ┴
typ └──────┘ ┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴┴┴
doc └──────┘
317 begin
st └─────
318 rw isometry_emetric_iff_metric,
id └─────────────────────────┘
src └─┘└─────────────────────────┘
typ └─┘└─────────────────────────┘
doc └─┘└─────────────────────────┘
txt └─┘
par └─┘
pid ┴
st ───────────────────────────────┘└─
319 split,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ──────┘└─
320 { assume H x,
src └────────┘
typ └────────┘
doc └────────┘
txt └────────┘
par └────────┘
pid └────────┘
st ───┘└────────┘└─
321 have := H x 0,
id ┴ ┴
src └──────┘ ┴ └┘
typ └──────┘┴┴┴└┘
doc └──────┘ ┴ └┘
txt └──────┘ ┴ └┘
par └──────┘ ┴ └┘
pid └───┘└─┘ ┴ ┴┴
st ────────────────┘└─
322 rwa [dist_eq_norm, dist_eq_norm, f.map_zero, sub_zero, sub_zero] at this },
id └──────────┘ └──────────┘ └──────┘ └──────┘
src └───┘└──────────┘└┘└──────────┘└┘ └┘└──────┘└┘└──────┘└────────┘
typ └───┘└──────────┘└┘└──────────┘└┘└────────┘└┘└──────┘└┘└──────┘└────────┘
doc └───┘ └┘ └┘ └┘ └┘ └────────┘
txt └───┘ └┘ └┘ └┘ └┘ └────────┘
par └───┘ └┘ └┘ └┘ └┘ └────────┘
pid └┘ └┘ └┘ └┘ └┘ ┴└──────┘┴
st ────────────────────┘└────────────┘└──────────┘└────────┘└────────┘┴└───────┘└┘└
323 { assume H x y,
src └──────────┘
typ └──────────┘
doc └──────────┘
txt └──────────┘
par └──────────┘
pid └──────────┘
st ───────────────┘└─
324 rw [dist_eq_norm, dist_eq_norm, ← f.map_sub, H] }
id └──────────┘ └──────────┘ ┴
src └──┘└──────────┘└┘└──────────┘└──┘ └┘ └┘
typ └──┘└──────────┘└┘└──────────┘└──┘└───────┘└┘┴└┘
doc └──┘ └┘ └──┘ └┘ └┘
txt └──┘ └┘ └──┘ └┘ └┘
par └──┘ └┘ └──┘ └┘ └┘
pid └┘ └┘ └──┘ └┘ ┴┴
st ───────────────────┘└────────────┘└───────────┘└─┘┴┴└─
325 end
st ──┘
326
327 variable (f)
328 /-- A continuous linear map is a uniform embedding if it expands the norm by a constant factor. -/
329 theorem uniform_embedding_of_bound (C : ℝ) (hC : ∀x, ∥x∥ ≤ C * ∥f x∥) :
id ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴┴ ┴┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴┴ ┴┴
330 uniform_embedding f :=
id └───────────────┘ ┴
src └───────────────┘
typ └───────────────┘ ┴
331 begin
st └─────
332 have Cpos : 0 < max C 1 := lt_of_lt_of_le zero_lt_one (le_max_right _ _),
id ┴ └─┘ ┴ └────────────┘ └─────────┘ └──────────┘
src └────────────┘┴┴└─┘┴ └────┘└────────────┘┴└─────────┘┴ └──────────┘└───┘
typ └────────────┘┴┴└─┘┴┴└────┘└────────────┘┴└─────────┘┴ └──────────┘└───┘
doc └────────────┘ ┴ ┴ └────┘ ┴ ┴ └───┘
txt └────────────┘ ┴ ┴ └────┘ ┴ ┴ └───┘
par └────────────┘ ┴ ┴ └────┘ ┴ ┴ └───┘
pid └───────┘└───┘ ┴ ┴ ┴└───┘ ┴ ┴ └───┘
st ─────────────────────────────────────────────────────────────────────────┘└─
333 refine uniform_embedding_iff'.2 ⟨metric.uniform_continuous_iff.1 f.uniform_continuous,
id └────────────────────┘ └───────────────────────────┘ └──────────────────┘
src └─────┘└────────────────────┘└─┘ └───────────────────────────┘└─┘└──────────────────┘└─
typ └─────┘└────────────────────┘└─┘ └───────────────────────────┘└─┘└──────────────────┘└─
doc └─────┘└────────────────────┘└─┘ └─┘└──────────────────┘└─
txt └─────┘ └─┘ └─┘ └─
par └─────┘ └─┘ └─┘ └─
pid ┴ └─┘ └─┘ └─
st ─────────────────────────────────────────────────────────────────────────────────────────
334 λδ δpos, ⟨δ / (max C 1), div_pos δpos Cpos, λx y hxy, _⟩⟩,
id ┴ └─┘ ┴ └─────┘ └──┘
src ───────────────────────────────────┘ └──────┘ ┴┴┴ └─┘┴ └───┘└─────┘┴ ┴ └┘ └──────────┘
typ ───────────────────────────────────┘ └──────┘ ┴┴┴ └─┘┴┴└───┘└─────┘┴ ┴└──┘└┘ └──────────┘
doc ───────────────────────────────────┘ └──────┘ ┴ ┴ ┴ └───┘ ┴ ┴ └┘ └──────────┘
txt ───────────────────────────────────┘ └──────┘ ┴ ┴ ┴ └───┘ ┴ ┴ └┘ └──────────┘
par ───────────────────────────────────┘ └──────┘ ┴ ┴ ┴ └───┘ ┴ ┴ └┘ └──────────┘
pid ───────────────────────────────────┘ └──────┘ ┴ ┴ ┴ └───┘ ┴ ┴ └┘ └──────────┘
st ────────────────────────────────────────────────────────────────────────────────────────────┘└─
335 calc dist x y = ∥x - y∥ : by rw dist_eq_norm
id └──┘ ┴ ┴ └──────────┘
src └──┘ └─┘└──────────┘└
typ └──┘ ┴ ┴ └─┘└──────────┘└
doc └──┘ └─┘ └
txt └─┘ └
par └─┘ └
pid ┴ └
st ─────────────────────────────┘└────────────────
336 ... ≤ C * ∥f (x - y)∥ : hC _
id ┴ ┴┴ ┴ ┴ └┘
src ─┘ ┴ ┴ ┴
typ ─┘ ┴ ┴┴ ┴ ┴ └┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└────────────────────────────
337 ... = C * dist (f x) (f y) : by rw [f.map_sub, dist_eq_norm]
id └──┘ └──────────┘
src └──┘ └──┘ └┘└──────────┘└─
typ └──┘ └──┘└───────┘└┘└──────────┘└─
doc └──┘ └┘ └─
txt └──┘ └┘ └─
par └──┘ └┘ └─
pid └┘ └┘ ┴└
st ────────────────────────────────┘└────────────┘└────────────┘┴└
338 ... ≤ max C 1 * dist (f x) (f y) :
id └─┘
src ─┘ └─┘
typ ─┘ └─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└──────────────────────────────────
339 mul_le_mul_of_nonneg_right (le_max_left _ _) dist_nonneg
id └────────────────────────┘ └─────────┘ └─────────┘
src └────────────────────────┘ └─────────┘ └─────────┘
typ └────────────────────────┘ └─────────┘ └─────────┘
st ─────────────────────────────────────────────────────────────
340 ... < max C 1 * (δ / max C 1) : mul_lt_mul_of_pos_left hxy Cpos
id ┴ └────────────────────┘ └─┘ └──┘
src ┴ └────────────────────┘
typ ┴ └────────────────────┘ └─┘ └──┘
st ──────────────────────────────────────────────────────────────────
341 ... = δ : by { rw mul_comm, exact div_mul_cancel _ (ne_of_lt Cpos).symm }
id ┴ └──────┘ └────────────┘ └──────┘ └──┘
src └─┘└──────┘ └────┘└────────────┘└─┘ └──────┘┴ └─────┘
typ ┴ └─┘└──────┘ └────┘└────────────┘└─┘ └──────┘┴└──┘└─────┘
doc └─┘ └────┘ └─┘ ┴ └─────┘
txt └─┘ └────┘ └─┘ ┴ └─────┘
par └─┘ └────┘ └─┘ ┴ └─────┘
pid ┴ ┴ └─┘ ┴ └───┘└┘
st ─────────────┘└────────────┘└────────────────────────────────────────────┘└─
342 end
st ──┘
343
344 /-- If a continuous linear map is a uniform embedding, then it expands the norm by a positive
345 factor.-/
346 theorem bound_of_uniform_embedding (hf : uniform_embedding f) :
id └───────────────┘ ┴
src └───────────────┘
typ └───────────────┘ ┴
347 ∃ C : ℝ, 0 < C ∧ ∀x, ∥x∥ ≤ C * ∥f x∥ :=
id ┴ ┴┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴┴ ┴┴
src ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴┴ ┴┴
348 begin
st └─────
349 obtain ⟨ε, εpos, hε⟩ : ∃ (ε : ℝ) (H : ε > 0), ∀ {x y : E}, dist (f x) (f y) < ε → dist x y < 1, from
id ┴ ┴ ┴ ┴ ┴ ┴ └──┘
src └─────────────────────┘┴└────┘ └─────┘ ┴┴└─┘┴┴ └──────┘ ┴ ┴ ┴ ┴ └┘ ┴ └┘┴┴ ┴ ┴└──┘┴ ┴ ┴ └┘ └────
typ └─────────────────────┘┴└────┘ └─────┘ ┴┴└─┘┴┴ └──────┘┴┴ ┴ ┴ ┴ └┘ ┴┴ └┘┴┴ ┴ ┴└──┘┴ ┴ ┴ └┘ └────
doc └─────────────────────┘ └────┘ └─────┘ ┴ └─┘ ┴ └──────┘ ┴ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └────
txt └─────────────────────┘ └────┘ └─────┘ ┴ └─┘ ┴ └──────┘ ┴ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └────
par └─────────────────────┘ └────┘ └─────┘ ┴ └─┘ ┴ └──────┘ ┴ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └────
pid └───────────────┘ └────┘ └─────┘ ┴ └─┘ ┴ └──────┘ ┴ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ └────
st ───────────────────────────────────────────────────────────────────────────────────────────────┘└──────
350 (uniform_embedding_iff.1 hf).2.2 1 zero_lt_one,
id └───────────────────┘ └┘ └─────────┘
src ───┘ └───────────────────┘└─┘ └──────┘└─────────┘
typ ───┘ └───────────────────┘└─┘└┘└──────┘└─────────┘
doc ───┘ └─┘ └──────┘
txt ───┘ └─┘ └──────┘
par ───┘ └─┘ └──────┘
pid ───┘ └─┘ └──────┘
st ─────────────────────────────────────────────────┘└─
351 let δ := ε/2,
id ┴┴
src └───────┘ ┴┴
typ └───────┘┴┴┴
doc └───────┘ ┴
txt └───────┘ ┴
par └───────┘ ┴
pid └───┘┴└─┘ ┴
st ─────────────┘└─
352 have δ_pos : δ > 0 := half_pos εpos,
id ┴ └──────┘ └──┘
src └───────────┘ ┴ └────┘└──────┘┴
typ └───────────┘┴┴ └────┘└──────┘┴└──┘
doc └───────────┘ ┴ └────┘ ┴
txt └───────────┘ ┴ └────┘ ┴
par └───────────┘ ┴ └────┘ ┴
pid └────────┘└─┘ ┴ ┴└───┘ ┴
st ────────────────────────────────────┘└─
353 have H : ∀{x}, ∥f x∥ ≤ δ → ∥x∥ ≤ 1,
id ┴┴ ┴ ┴ ┴
src └───────┘ └─┘ ┴┴ ┴ ┴┴┴┴ ┴ ┴ ┴ └┘
typ └───────┘ └─┘ ┴┴┴┴ ┴┴┴┴┴┴ ┴ ┴ └┘
doc └───────┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘
txt └───────┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘
par └───────┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘
pid └────┘└─┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴
st ───────────────────────────────────┘└─
354 { assume x hx,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └─────────┘
st ───┘└─────────┘└─
355 have : dist x 0 ≤ 1,
id └──┘ ┴
src └─────┘└──┘┴ └─┘ └┘
typ └─────┘└──┘┴┴└─┘ └┘
doc └─────┘ ┴ └─┘ └┘
txt └─────┘ ┴ └─┘ └┘
par └─────┘ ┴ └─┘ └┘
pid └───┘└┘ ┴ └─┘ ┴┴
st ──────────────────────┘└─
356 { apply le_of_lt,
id └──────┘
src └────┘└──────┘
typ └────┘└──────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ─────┘└────────────┘└─
357 apply hε,
src └────┘
typ └────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ─────────────┘└─
358 simp [dist_eq_norm],
id └──────────┘
src └────┘└──────────┘┴
typ └────┘└──────────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴┴ ┴
st ────────────────────────┘└─
359 exact lt_of_le_of_lt hx (half_lt_self εpos) },
id └────────────┘ └┘ └──────────┘ └──┘
src └────┘└────────────┘┴ ┴ └──────────┘┴ └┘
typ └────┘└────────────┘┴└┘┴ └──────────┘┴└──┘└┘
doc └────┘ ┴ ┴ ┴ └┘
txt └────┘ ┴ ┴ ┴ └┘
par └────┘ ┴ ┴ ┴ └┘
pid ┴ ┴ ┴ ┴ ┴┴
st ─────────────────────────────────────────────────┘└┘└
360 simpa using this },
id └──┘
src └──────────┘ ┴
typ └──────────┘└──┘┴
doc └──────────┘ ┴
txt └──────────┘ ┴
par └──────────┘ ┴
pid ┴└────┘ ┴
st ──────────────────┘└┘└
361 rcases normed_field.exists_one_lt_norm 𝕜 with ⟨c, hc⟩,
id └─────────────────────────────┘ ┴
src └─────┘└─────────────────────────────┘┴ └───────────┘
typ └─────┘└─────────────────────────────┘┴┴└───────────┘
doc └─────┘ ┴ └───────────┘
txt └─────┘ ┴ └───────────┘
par └─────┘ ┴ └───────────┘
pid ┴ ┴ └───────────┘
st ──────────────────────────────────────────────────────┘└─
362 refine ⟨δ⁻¹ * ∥c∥, (mul_pos (inv_pos δ_pos) ((lt_trans zero_lt_one hc))), (λx, _)⟩,
id ┴└┘ ┴ ┴ └─────┘ └─────┘ └───┘ └──────┘ └─────────┘ └┘
src └─────┘ └┘┴┴┴ └┘ └─────┘┴ └─────┘┴ └┘ └──────┘┴└─────────┘┴ └───┘ └────┘
typ └─────┘ ┴└┘┴┴┴ ┴ └┘ └─────┘┴ └─────┘┴└───┘└┘ └──────┘┴└─────────┘┴└┘└───┘ └────┘
doc └─────┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └───┘ └────┘
txt └─────┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └───┘ └────┘
par └─────┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └───┘ └────┘
pid ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └───┘ └────┘
st ───────────────────────────────────────────────────────────────────────────────────┘└─
363 by_cases hx : f x = 0,
id ┴ ┴ ┴
src └───────┘ └─┘ ┴ ┴┴└┘
typ └───────┘ └─┘┴┴┴┴┴└┘
doc └───────┘ └─┘ ┴ ┴ └┘
txt └───────┘ └─┘ ┴ ┴ └┘
par └───────┘ └─┘ ┴ ┴ └┘
pid ┴ └─┘ ┴ ┴ ┴┴
st ──────────────────────┘└─
364 { have : f x = f 0, by { simp [hx] },
id ┴ ┴
src └─────┘ ┴ ┴ ┴ └┘
typ └─────┘ ┴┴┴ ┴┴└┘
doc └─────┘ ┴ ┴ ┴ └┘
txt └─────┘ ┴ ┴ ┴ └┘
par └─────┘ ┴ ┴ ┴ └┘
pid └───┘└┘ ┴ ┴ ┴ ┴┴
st ───┘└──────────────┘ └┘
365 have : x = 0 := (uniform_embedding_iff.1 hf).1 this,
id ┴
typ ┴
366 simp [this] },
st └┘
367 { rcases rescale_to_shell hc δ_pos hx with ⟨d, hd, dxle, ledx, dinv⟩,
368 have : ∥f (d • x)∥ ≤ δ, by simpa,
id ┴ ┴ ┴
typ ┴ ┴ ┴
369 have : ∥d • x∥ ≤ 1 := H this,
id ┴ ┴
typ ┴ ┴
370 calc ∥x∥ = ∥d∥⁻¹ * ∥d • x∥ :
id ┴ ┴
typ ┴ ┴
371 by rwa [← normed_field.norm_inv, ← norm_smul, ← mul_smul, inv_mul_cancel, one_smul]
372 ... ≤ ∥d∥⁻¹ * 1 :
373 mul_le_mul_of_nonneg_left this (inv_nonneg.2 (norm_nonneg _))
374 ... ≤ δ⁻¹ * ∥c∥ * ∥f x∥ :
id ┴ ┴
typ ┴ ┴
375 by rwa [mul_one] }
st └─
376 end
st ──┘
377
378 section uniformly_extend
379
380 variables [complete_space F] (e : E →L[𝕜] G) (h_dense : dense_range e)
381
382 section
383 variables (h_e : uniform_inducing e)
384
385 /-- Extension of a continuous linear map `f : E →L[𝕜] F`, with `E` a normed space and `F` a complete
386 normed space, along a uniform and dense embedding `e : E →L[𝕜] G`. -/
387 def extend : G →L[𝕜] F :=
id ┴ ┴ ┴
typ ┴ ┴ ┴
388 /- extension of `f` is continuous -/
389 have cont : _ := (uniform_continuous_uniformly_extend h_e h_dense f.uniform_continuous).continuous,
390 /- extension of `f` agrees with `f` on the domain of the embedding `e` -/
391 have eq : _ := uniformly_extend_of_ind h_e h_dense f.uniform_continuous,
392 { to_fun := (h_e.dense_inducing h_dense).extend f,
393 add :=
394 begin
395 refine is_closed_property2 h_dense (is_closed_eq _ _) _,
396 { exact cont.comp (continuous_fst.add continuous_snd) },
st └┘
397 { exact (cont.comp continuous_fst).add (cont.comp continuous_snd) },
st └┘
398 { assume x y, rw ← e.map_add, simp only [eq], exact f.map_add _ _ },
st └┘
399 end,
st └─┘
400 smul := λk,
id ┴
typ ┴
401 begin
402 refine is_closed_property h_dense (is_closed_eq _ _) _,
403 { exact cont.comp (continuous_const.smul continuous_id) },
st └┘
404 { exact (continuous_const.smul continuous_id).comp cont },
st └┘
405 { assume x, rw ← map_smul, simp only [eq], exact map_smul _ _ _ },
st └┘
406 end,
st └─┘
407 cont := cont
408 }
409
410 @[simp] lemma extend_zero : extend (0 : E →L[𝕜] F) e h_dense h_e = 0 :=
id ┴ ┴ ┴
typ ┴ ┴ ┴
doc └──┘
411 begin
412 apply ext,
413 refine is_closed_property h_dense (is_closed_eq _ _) _,
414 { exact (uniform_continuous_uniformly_extend h_e h_dense uniform_continuous_const).continuous },
st └┘
415 { simp only [zero_apply], exact continuous_const },
st └┘
416 { assume x, exact uniformly_extend_of_ind h_e h_dense uniform_continuous_const x }
id ┴
typ ┴
st └─
417 end
st ──┘
418
419 end
420
421 section
422 variables {N : ℝ} (h_e : ∀x, ∥x∥ ≤ N * ∥e x∥)
id ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴
423
424 local notation `ψ` := f.extend e h_dense (uniform_embedding_of_bound _ _ h_e).to_uniform_inducing
425
426 /-- If a dense embedding `e : E →L[𝕜] G` expands the norm by a constant factor `N⁻¹`, then the norm
427 of the extension of `f` along `e` is bounded by `N * ∥f∥`. -/
428 lemma op_norm_extend_le : ∥ψ∥ ≤ N * ∥f∥ :=
id ┴
typ ┴
429 begin
430 have uni : uniform_inducing e := (uniform_embedding_of_bound _ _ h_e).to_uniform_inducing,
431 have eq : ∀x, ψ (e x) = f x := uniformly_extend_of_ind uni h_dense f.uniform_continuous,
id ┴
typ ┴
432 by_cases N0 : 0 ≤ N,
id ┴
typ ┴
433 { refine op_norm_le_bound ψ _ (is_closed_property h_dense (is_closed_le _ _) _),
434 { exact mul_nonneg N0 (norm_nonneg _) },
st └┘
435 { exact continuous_norm.comp (cont ψ) },
st └┘
436 { exact continuous_const.mul continuous_norm },
st └┘
437 { assume x,
438 rw eq,
439 calc ∥f x∥ ≤ ∥f∥ * ∥x∥ : le_op_norm _ _
440 ... ≤ ∥f∥ * (N * ∥e x∥) : mul_le_mul_of_nonneg_left (h_e x) (norm_nonneg _)
id ┴
typ ┴
441 ... ≤ N * ∥f∥ * ∥e x∥ : by rw [mul_comm N ∥f∥, mul_assoc] } },
id ┴ ┴
typ ┴ ┴
st ┴ └──┘
442 { have he : ∀ x : E, x = 0,
id ┴
typ ┴
443 { assume x,
444 have N0 : N ≤ 0 := le_of_lt (lt_of_not_ge N0),
id ┴
typ ┴
445 rw ← norm_le_zero_iff,
446 exact le_trans (h_e x) (mul_nonpos_of_nonpos_of_nonneg N0 (norm_nonneg _)) },
id ┴
typ ┴
st └┘
447 have hf : f = 0, { ext, simp only [he x, zero_apply, map_zero] },
id ┴
typ ┴
st └┘
448 have hψ : ψ = 0, { rw hf, apply extend_zero },
st └┘
449 rw [hψ, hf, norm_zero, norm_zero, mul_zero] }
st ┴ └─
450 end
st ──┘
451
452 end
453
454 end uniformly_extend
455
456 end op_norm
457
458 /-- The norm of the tensor product of a scalar linear map and of an element of a normed space
459 is the product of the norms. -/
460 @[simp] lemma smul_right_norm {c : E →L[𝕜] 𝕜} {f : F} :
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
doc └──┘
461 ∥smul_right c f∥ = ∥c∥ * ∥f∥ :=
id ┴ ┴
typ ┴ ┴
462 begin
463 refine le_antisymm _ _,
464 { apply op_norm_le_bound _ (mul_nonneg (norm_nonneg _) (norm_nonneg _)) (λx, _),
id ┴
typ ┴
465 calc
466 ∥(c x) • f∥ = ∥c x∥ * ∥f∥ : norm_smul _ _
id ┴ ┴
typ ┴ ┴
467 ... ≤ (∥c∥ * ∥x∥) * ∥f∥ :
468 mul_le_mul_of_nonneg_right (le_op_norm _ _) (norm_nonneg _)
469 ... = ∥c∥ * ∥f∥ * ∥x∥ : by ring },
st └┘
470 { by_cases h : ∥f∥ = 0,
id ┴
typ ┴
471 { rw h, simp [norm_nonneg] },
st └┘
472 { have : 0 < ∥f∥ := lt_of_le_of_ne (norm_nonneg _) (ne.symm h),
id ┴
typ ┴
473 rw ← le_div_iff this,
474 apply op_norm_le_bound _ (div_nonneg (norm_nonneg _) this) (λx, _),
id ┴
typ ┴
475 rw [div_mul_eq_mul_div, le_div_iff this],
476 calc ∥c x∥ * ∥f∥ = ∥c x • f∥ : (norm_smul _ _).symm
id ┴ ┴
typ ┴ ┴
477 ... = ∥((smul_right c f) : E → F) x∥ : rfl
id ┴ ┴
typ ┴ ┴
478 ... ≤ ∥smul_right c f∥ * ∥x∥ : le_op_norm _ _ } },
st └──┘
479 end
st └─┘
480
481 section restrict_scalars
482
483 variable (𝕜)
484 variables {𝕜' : Type*} [normed_field 𝕜'] [normed_algebra 𝕜 𝕜']
id └──────────┘
src └──────────┘
typ └──────────┘
doc └──────────┘
485 {E' : Type*} [normed_group E'] [normed_space 𝕜' E']
id └──────────┘
src └──────────┘
typ └──────────┘
doc └──────────┘
486 {F' : Type*} [normed_group F'] [normed_space 𝕜' F']
id └──────────┘
src └──────────┘
typ └──────────┘
doc └──────────┘
487
488 local attribute [instance, priority 500] normed_space.restrict_scalars
id └───────────────────────────┘
src └───────────────────────────┘
typ └───────────────────────────┘
doc └───────────────────────────┘
489
490 /-- `𝕜`-linear continuous function induced by a `𝕜'`-linear continuous function when `𝕜'` is a
491 normed algebra over `𝕜`. -/
492 def restrict_scalars (f : E' →L[𝕜'] F') : E' →L[𝕜] F' :=
id └┘ └─┘└┘┴ └┘ └┘ └─┘┴┴ └┘
src └─┘ ┴ └─┘ ┴
typ └┘ └─┘└┘┴ └┘ └┘ └─┘┴┴ └┘
doc └─┘ ┴ └─┘ ┴
493 { cont := f.cont,
id ┴└───┘
src └───┘
typ ┴└───┘
494 ..linear_map.restrict_scalars 𝕜 (f.to_linear_map) }
id └─────────────────────────┘ ┴ ┴└────────────┘
src └─────────────────────────┘ └────────────┘
typ └─────────────────────────┘ ┴ ┴└────────────┘
doc └─────────────────────────┘
495
496 @[simp, move_cast] lemma restrict_scalars_coe_eq_coe (f : E' →L[𝕜'] F') :
id └┘ └─┘└┘┴ └┘
src └─┘ ┴
typ └┘ └─┘└┘┴ └┘
doc └──┘ └───────┘ └─┘ ┴
497 (f.restrict_scalars 𝕜 : E' →ₗ[𝕜] F') = (f : E' →ₗ[𝕜'] F').restrict_scalars 𝕜 := rfl
id ┴└───────────────┘ ┴ └┘ └─┘┴┴ └┘ ┴ ┴ └┘ └─┘└┘┴ └┘ └──────────────┘ ┴ └─┘
src └───────────────┘ └─┘ ┴ ┴ └─┘ ┴ └──────────────┘ └─┘
typ ┴└───────────────┘ ┴ └┘ └─┘┴┴ └┘ ┴ ┴ └┘ └─┘└┘┴ └┘ └──────────────┘ ┴ └─┘
doc └───────────────┘ └──────────────┘
498
499 @[simp, squash_cast] lemma restrict_scalars_coe_eq_coe' (f : E' →L[𝕜'] F') :
id └┘ └─┘└┘┴ └┘
src └─┘ ┴
typ └┘ └─┘└┘┴ └┘
doc └──┘ └─────────┘ └─┘ ┴
500 (f.restrict_scalars 𝕜 : E' → F') = f := rfl
id ┴└───────────────┘ ┴ └┘ └┘ ┴ ┴ └─┘
src └───────────────┘ ┴ └─┘
typ ┴└───────────────┘ ┴ └┘ └┘ ┴ ┴ └─┘
doc └───────────────┘
501
502 end restrict_scalars
503
504 end continuous_linear_map
505
506 /-- If both directions in a linear equiv `e` are continuous, then `e` is a uniform embedding. -/
507 lemma linear_equiv.uniform_embedding (e : E ≃ₗ[𝕜] F) (h₁ : continuous e) (h₂ : continuous e.symm) :
id ┴ └─┘┴┴ ┴ └────────┘ ┴ └────────┘ ┴└───┘
src └─┘ ┴ └────────┘ └────────┘ └───┘
typ ┴ └─┘┴┴ ┴ └────────┘ ┴ └────────┘ ┴└───┘
doc └─┘ ┴ └────────┘ └────────┘ └───┘
508 uniform_embedding e :=
id └───────────────┘ ┴
src └───────────────┘
typ └───────────────┘ ┴
509 begin
510 rcases linear_map.bound_of_continuous e.symm.to_linear_map h₂ with ⟨C, Cpos, hC⟩,
511 let f : E →L[𝕜] F := { cont := h₁, ..e },
512 apply f.uniform_embedding_of_bound C (λx, _),
513 have : e.symm (e x) = x := linear_equiv.symm_apply_apply _ _,
514 conv_lhs { rw ← this },
515 exact hC _
516 end
st └─┘
517
518 /-- If a continuous linear map is constructed from a linear map via the constructor `mk_continuous`,
519 then its norm is bounded by the bound given to the constructor if it is nonnegative. -/
520 lemma linear_map.mk_continuous_norm_le (f : E →ₗ[𝕜] F) {C : ℝ} (hC : 0 ≤ C) (h : ∀x, ∥f x∥ ≤ C * ∥x∥) :
id ┴ └─┘┴┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴ ┴┴┴
src └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ └─┘┴┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴ ┴┴┴
521 ∥f.mk_continuous C h∥ ≤ C :=
id ┴┴└────────────┘ ┴ ┴┴ ┴ ┴
src ┴ └────────────┘ ┴ ┴
typ ┴┴└────────────┘ ┴ ┴┴ ┴ ┴
doc └────────────┘
522 continuous_linear_map.op_norm_le_bound _ hC h